Nuprl Lemma : ma-rframe_wf
0,22
postcript
pdf
M
:MsgA,
k
:Knd,
x
:Id.
M
.rframe(
k
reads
x
)
Prop
latex
Definitions
Knd
,
t
T
,
Id
,
type
List
,
x
.
A
(
x
)
,
x
:
A
.
B
(
x
)
,
x
.
t
(
x
)
,
Top
,
a
:
A
fp
B
(
a
)
,
x
:
A
B
(
x
)
,
IdDeq
,
x
dom(
f
)
,
b
,
Type
,
{
x
:
A
|
B
(
x
) }
,
KindDeq
,
deq-member(
eq
;
x
;
L
)
,
Prop
,
x
,
y
.
t
(
x
;
y
)
,
z
!=
f
(
x
)
P
(
a
;
z
)
,
M
.rframe(
k
reads
x
)
,
x
:
A
B
(
x
)
,
MsgA
Lemmas
msga
wf
,
fpf-val
wf
,
deq-member
wf
,
Kind-deq
wf
,
assert
wf
,
fpf-dom
wf
,
id-deq
wf
,
fpf-trivial-subtype-top
,
Id
wf
,
Knd
wf
origin
M:MsgA, k:Knd, x:Id. M.rframe(k reads x) 
Prop M:MsgA, k:Knd, x:Id. M.rframe(k reads x) Prop T
x.A(x)x:A. B(x)
x. t(x)
B(a)
B(x) dom(f)
bx,y. t(x;y)
P(a;z)
B(x)